package controller.solver;

import java.io.BufferedReader;
import java.io.File;
import java.io.IOException;
import java.io.InputStreamReader;
import java.util.Scanner;

import model.solver.RSatParameter;
import model.solver.SolverParameter;
import model.solver.SolverResult;
import model.solver.SolverResultStatus;

/**
 * This class is a implementation of Solver for RSat
 * 
 * @author stephane
 *
 */
public class RSat extends Solver {

	public static final String EXEC = "rsat";
	public static final String DESCRIPTION = "Result of the minisat execution";
		
	public static final String UNKNOW_TOKEN = "UNKNOW";
	public static final String DECISION_TOKEN = "Decisions: ";
	public static final String CONFLICT_TOKEN = "Conflicts: ";
	public static final String BEGIN_PRINT_TOKEN = "\nv";
	public static final String END_PRINT_TOKEN = "\nc";
	
	//public static final int DEFAULT_RETURN_VALUE = 0; 
	public static final int RETURN_UNSATISFIABLE = 20;
	public static final int RETURN_SATISFIABLE = 10;


	public static final int DEFAULT_NB_PARAM = 2;
	public static final int NB_PARAM_TIMEOUT = 2;
	public static final int NB_PARAM_PRINT_SOLUTION = 1;
	
	
	private RSatParameter param;
	
	
	public RSat(File directory) throws IOException {
		if(!directory.isDirectory() || ! new File(directory, EXEC).isFile())
			throw new IllegalArgumentException();
		
		param = new RSatParameter();
		try {
			path = directory.getCanonicalPath() + File.separator + EXEC;
		} catch (IOException e) {
			e.printStackTrace();
			throw new IOException();
		}
	}

	@Override
	public boolean checkParameter() {
		return param.basicCheck();
	}

	@Override
	public SolverParameter getSolverParameter() {
		return param;
	}

	public RSatParameter getRSatParameter() {
		return param;
	}
	
	@Override
	public String[] getCommandLine(String cnfFile) {
		// TODO ajouter les autre arg
		String[] tab ;
		int nbParam = DEFAULT_NB_PARAM;
		
		if(param.needTimeOut())
			nbParam += NB_PARAM_TIMEOUT;
		if(param.isPrintSolution())
			nbParam += NB_PARAM_PRINT_SOLUTION;
		
		tab = new String[nbParam];
		
		int nb = 0;
		//bash
		tab[nb++] = path;
		//stdin
		tab[nb++] = cnfFile;//correctFormatForLinux(cnfFile);
		if(param.needTimeOut())
		{//gere timeout
			tab[nb++] = "-t";
			tab[nb++] = String.valueOf(param.getTimeOut() / 1000);
		}
		if(param.isPrintSolution())
		{//gere impresison de la solution
			tab[nb++] = "-s";
		}
		
		return tab;
	}

	@Override
	public boolean hasTimeout() {
		return true;
	}

	@Override
	public SolverResult runSolver(String[] cmd) {
		// TODO copier coller
		SolverResult res = new SolverResult(); 
		
		BufferedReader input = null;
		BufferedReader inerr = null;
		try{//lance le processus
			res.setBegin(System.currentTimeMillis());
			
			process = Runtime.getRuntime().exec(cmd);

			String line;
			input = new BufferedReader (new InputStreamReader(process.getInputStream()));
			inerr = new BufferedReader (new InputStreamReader(process.getErrorStream()));
			
			while ((line = input.readLine()) != null) 
			{ //verifie les stdin
				System.out.println(line);
				res.addStdin(line+"\n");
			}
			while ((line = inerr.readLine()) != null) 
			{ //verifie les stderr
				System.out.println(line);
				res.addStderr(line+"\n");
			}
		}
		catch(IOException e){
			//e.printStackTrace();
			res.setStatus(SolverResultStatus.PROBLEM);
			if(process != null)
				process.destroy();
		}
		finally{
			try{
				if(input != null)
					input.close();
				if(inerr != null)
					inerr.close();
				if(process != null)
					res.setExitVal(process.waitFor());
			}
			catch(Exception e){
				e.printStackTrace();
				res.setStatus(SolverResultStatus.PROBLEM);
			}
			
		}
		//terminer
		res.setEnd(System.currentTimeMillis());

		System.out.println("val de retour "+res.getExitVal());
		
		//s'occupe du status
		if(res.getStdin().indexOf(UNKNOW_TOKEN) != -1)
			res.setStatus(SolverResultStatus.TIMEOUT_REACHED);
		else
			if(res.getStatus() == SolverResultStatus.PROBLEM)
				switch(res.getExitVal()){
				case RETURN_UNSATISFIABLE : 
					res.setStatus(SolverResultStatus.UNSATISFIABLE); 
					setLastResult(res);
					break ;
				case RETURN_SATISFIABLE :
					res.setStatus(SolverResultStatus.SATISFIABLE) ;
					setLastResult(res);
					break ;
				
				default : res.setStatus(SolverResultStatus.PROBLEM) ; 
				}
					
		//dernier details
		res.setDescription(DESCRIPTION);
		
		return res;
	}

	private void setLastResult(SolverResult res){
		int index = res.getStdin().indexOf(BEGIN_PRINT_TOKEN);
		if(index != -1)
		{//recupere l solution
			String tmp = res.getStdin().substring(index + BEGIN_PRINT_TOKEN.length());
			int indexFin = tmp.indexOf(END_PRINT_TOKEN);
			
			res.setSolution(tmp.substring(0, indexFin));
		}
		
		//recupere details
		index = res.getStdin().indexOf(DECISION_TOKEN);
		Scanner scan = new Scanner(res.getStdin().substring(index + DECISION_TOKEN.length()));
		
		//recupere le nb de decision
		res.setDecisions(scan.nextInt());
		
		//recupere le nb de conflict
		index = res.getStdin().indexOf(CONFLICT_TOKEN);
		scan = new Scanner(res.getStdin().substring(index + CONFLICT_TOKEN.length()));
		res.setConflics(scan.nextInt());
	}

}
